(declare-fun v1 () Bool)
(declare-fun i2 () Int)
(declare-fun str1 () String)
(declare-fun str6 () String)
(declare-fun str7 () String)
(declare-fun str8 () String)
(assert (= 17 (str.to_int str1)))
(push)
(assert (or (= (str.++ str7 str1) (ite (= 1 (+ i2 (str.to_int str1))) (str.++ str6 str6 str7) str8)) v1))
(push)
(assert v1)
(check-sat)
